Step of Proof: multiply_nat_wf 12,41
Inference at * 2 0 1 2 1 1 
Iof proof for Lemma multiply nat wf:

.....basecase..... NILNIL

1. i : 
  0  (i * 0) 
latex
 by Id  
latex

 1: .....basecase..... NILNIL

 1:   0  (i * 0)
 .

origin